CS60030 Formal Systems SPRING 2023, L-T-P: 3-1-0

Schedule

Instructor     Prof. Pallab Dasgupta
Timing     Wed 10:00 -11:00
Thu 9:00 - 10:00
Fri 11:00 - 13:00
Venue     CSE Room No: 108
Teaching Assistants     Sourav Das (sourav.iniesta13@gmail.com),
Briti Gangopadhay (briti.tana@gmail.com)
  

Syllabus

  • Introduction
  • Succinct Representations
  • Symbolic Reachability
  • Specification Formalisms
  • Omega Regular Languages and Buchi Automata
  • Model Checking
  • Scalability in Model Checking
  • Program Verification
  • Timed Automata
  • Hybrid Automata

Books and References

    [1]     Pallab Dasgupta A Roadmap for Formal Property Verification, Springer, 2006
    [2]     Christel Baier and Joost-Pieter Katoen Principles of Model Checking, MIT Press, 2008.
    [3]     Edmund M. Clarke, Thomas A. Henzinger, Helmut Veith, Roderick Bloem Handbook of Model Checking, Springer, 2019
    [4]     Rajeev Alur Principles of Cyber-Physical Systems, MIT Press, 2015

Online Material

Week Topic Chapter PDF Tutorial
Week 1
Introduction Introduction Introduction
Succinct Representations Succinct Representations Succinct Representations
Week 2 Symbolic Reachability Symbolic Reachability Symbolic Reachability
Week 3 Hands on SAT Hands on SAT - Tutorial SAT
Tutorial SAT and BDD Tutorial SAT and BDD - Tutorial SAT and BDD
Week 4 Omega Regular Languages and Buchi Automata Omega Regular Languages and Buchi Automata Omega Regular Languages and Buchi Automata
Week 5 Tutorial on Symbolic Reachability and Omega Regular Languages Tutorial on Symbolic Reachability and Omega Regular Languages - Tutorial on Symbolic Reachability and Omega Regular Languages
Week 6 Specification Formalisms Specification Formalisms Specification Formalisms -
Week 7 Model Checking Model Checking Model Checking
Tutorial 4 LTL, CTL and Model Checking - Tutorial on LTL, CTL and Model Checking
Week 8 Scalability in Model Checking Scalability in Model Checking Scalability in Model Checking
Program Verification Program Verification Program Verification
Week 9 Bounded Model Checking Bounded Model Checking Bounded Model Checking
Induction Interpolation PDR Induction Interpolation PDR Induction Interpolation PDR
Week 10 Timed Automata Timed Automata Timed Automata
Week 11 Tutorial TIMED AUTOMATA & HYBRID SYSTEMS Tutorial: Timed Automata & Hybrid Systems
Week 12 Hybrid Automata Hybrid Automata Hybrid Automata

Previous course pages: 2021 | 2020 | 2019

 CS60030 Formal Systems Spring 2023, L-T-P: 3-1-0